; <lemma>
;  <title>BoschSwitch.5</title>
;  <origin>BoschSwitch | m1 | TriggerOn/inv6/INV</origin>
(benchmark boschswitch_5
;  <theories>
;    <theory name="linear_order_int"/>
;  </theories>
  :logic QF_LIA
;  <typenv>
;    <variable name="CT" type="INTEGER"/>
;  </typenv>
  :extrafuns (
	       (CT Int) 
	       )
  :extramacros (
		 (Nat
		  (lambda (?i Int) . (<= 0 ?i)))
		 (in (lambda (?x 't) (?p ('t boolean)) . (?p ?x)))
		 )
; <hypothesis needed="true">CT : NATURAL</hypothesis>
  :assumption (in CT Nat)
  :formula
; <goal>0 <= CT</goal>
  (not
      (<= 0 CT)
    )
)
;</lemma>
